$\forall$$a$:Id, $T$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:Top, $x$:Id, $L$:Top, $t$:Type.
\\[0ex]${\it ds}$ $\parallel$ $x$ : $t$
\\[0ex]$\Rightarrow$ ((with ds: ${\it ds}$ action $a$:$T$ precondition $a$(v) is $P$ s v) $\Vert\!+$ only members of $L$ affect $x$ :$t$)